Step of Proof: p-id_wf 11,40
Inference at * 
Iof proof for Lemma p-id wf:


  T:Type. p-id()  T(T + Top) 
latex
 by (Unfold `p-id` ( 0)) 
CollapseTHEN (Auto) 
latex

C.

Definitionsp-id(), x:A. B(x), x.A(x), inl x , Top, t  T, Type
Lemmastop wf

origin